es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C.
 (m:E. ([m: sndr is_req   rcvr]  [m: rcvr is_ack  sndr]))
  (m:E
  ((([m: sndr is_req   rcvr]  [m: rcvr is_ack  sndr])
  (& (y:E.
  (& (([y: sndr is_req   rcvr]  [y: rcvr is_ack  sndr])
  (& ( ((y = m)  (z:E. f2f+-pred(z,y))))))) 

latex

Definitions

f2f+-pred(e',e), [e: i p j], P  Q, P  Q, SQType(T), {T}, x(s), A c B, , t  T, P & Q, P  Q, x:A. B(x), P  Q, x:A. B(x), [e: i p j], e(e1,e2].P(e), (e <loc e'), False, A, a = b, x  {FDLNOr12445}, Dec(P)

Lemmas

es-causle weakening locl, es-causle wf, decidable rcv-it, rcv-it wf, max-of-eventset, acks-between-reqs, es-causl weakening, es-locl-total, assert-eq-id, Id wf, Id sq, loc-of-req-sender, decidable es-E-equal, f2f+-pred wf, not wf, es-causl wf, decidable snd-it, es-minimal-event, req-sent-before-ack, ack-has-f2f+-pred, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, plus-ify wf, fifoC wf, f2f+Ack wf, f2f+Req wf, snd-it wf, es-E wf, f2f+-property